COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDCONST Table ε Blocks
C00004 ENDMK
C⊗;
DECLARE INDCONST Table ε Blocks;

DECLARE INDVAR s s1 s2 s3 s4 ε Situations;

DECLARE INDVAR x y z x1 y1 z1 x2 y2 z2 ε Blocks;

DECLARE PREDCONST clear(Blocks,Situations);

DECLARE OPCONST move(Blocks,Blocks,Situations) = Situations;

DECLARE OPCONST support(Blocks,Situations) = Blocks;

AXIOM TABLE:	∀x s.(¬support(Table,s) = x);;

AXIOM CLEAR:	∀x s.(clear(x,s) ≡ ∀y.(¬y=support(x,s)));;

AXIOM MOVE:	∀x y z s s1.(clear(x,s) ∧ (clear(y,s) ∨ y = Table)
∧ s1 = move(x,y,s) ∧ ¬(y=x) ∧ ¬(z=x) ⊃ support(x,s1) = y
∧ support(z,s1) = support(z,s));;


DECLARE INDCONST A B C ε Blocks;

AXIOM ALL:	∀x.(x=A ∨ x=B ∨ x=C ∨ x=Table);;

AXIOM DISTINCT:	¬(A=B)∧¬(A=C)∧¬(A=Table)∧¬(B=C)∧¬(B=Table)∧¬(C=Table);;

DECLARE INDCONST S0 ε Situations;

AXIOM INITIAL: support(C,S0) = B ∧ support(B,S0) = Table ∧ support(A,S0)=Table;;